COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Dear Dan:
C00006 ENDMK
C⊗;
Dear Dan:

	Including circumscription in the list of formalisms
requiring "non-constructive" proofs is mistaken.  Circumscribing a
formula generates an axiom schema, and whether a sentence can be obtained
by circumscription combined with the usual predicate calculus rules of
inference is just as semi-decidable as whether it is provable in
predicate calculus.  Whether a circumscription leads to true statements is
not well defined, because this depends on facts about the world not
expressed in the sentences.  This is as it should be, since
circumscription is a rule of conjecture, not a rule of inference.

	The main point of my Addendum is to point out that circumscription
differs from the other two in using axiom schemata and I had in mind
remarking that this therefore made it semi-decidable, but I see that
I neglected to make this point explicit.  I also pointed out that
schema-based versions of McDermott-Doyle and Reiter were sometimes
possible, but again neglected to say that this would make them
semi-decidable too.

	Your "clear reason for this problem" seems correct but misleading.
The true sentences of arithmetic are also not semi-decidable, but Peano
arithmetic, which is semi-decidable, is enough for most purposes.  Similarly,
circumscription is only an approximation to minimal models, but should
be satisfactory except in exotic cases.  Semi-decidable approximations
to McDermott-Doyle and Reiter should be possible in more general
circumstances than my Addendum proposes.

	Formula (3) of the Addendum is wrong.  The wff on(train,tracks)
should be replaced by PHI(train,tracks), i.e. the Greek letter not "PHI".

	Incidentally, while I still think that a "lack of oars" needs
to be included in the ontology of an intelligent program, it turns out
to be neater to do the circumscriptions involved in conjecturing that
one can cross the river without it.

	Perhaps I am partly responsible for this misclassification,
because minimal entailment, like entailment itself, is a semantic concept
and not semi-decidable, and you probably relied on early versions of the
paper.